import dbc.Pre;
import dbc.Post;

public class TestScript {

	public int x;
	
	public static void main(String[] args) {
		TestScript t = new TestScript();
		t.n(5, 4);
        t.n(-5, 4);
		t.n(1, -4);
        t.n(1, 4);
	}
	
	@Pre("i > 0")
	@Post("$return > 0 && $this.x == $old($this.x) + 1")
	public int n(int i, int j) {
		x += i;
		return j;
	}
}